Problem:
0(1(0(1(x1)))) -> 0(0(2(1(3(1(x1))))))
0(1(0(1(x1)))) -> 2(1(0(2(0(1(x1))))))
0(1(0(1(x1)))) -> 2(1(3(1(0(0(x1))))))
4(1(0(1(x1)))) -> 1(0(4(2(1(x1)))))
4(1(0(1(x1)))) -> 4(1(0(2(1(x1)))))
4(1(0(1(x1)))) -> 0(2(1(3(4(1(x1))))))
4(1(0(1(x1)))) -> 0(4(2(1(3(1(x1))))))
4(1(0(1(x1)))) -> 1(0(2(4(1(3(x1))))))
4(1(0(1(x1)))) -> 1(0(4(2(2(1(x1))))))
4(1(0(1(x1)))) -> 1(0(4(5(2(1(x1))))))
4(1(0(1(x1)))) -> 4(0(2(1(3(1(x1))))))
4(1(0(1(x1)))) -> 4(1(0(2(1(3(x1))))))
4(1(0(1(x1)))) -> 4(1(3(0(2(1(x1))))))
4(1(1(1(x1)))) -> 4(1(3(1(3(1(x1))))))
4(3(0(1(x1)))) -> 0(2(1(3(4(x1)))))
4(3(0(1(x1)))) -> 0(2(4(1(3(x1)))))
4(3(0(1(x1)))) -> 0(4(2(1(3(x1)))))
4(3(0(1(x1)))) -> 3(0(4(2(1(x1)))))
4(3(0(1(x1)))) -> 3(4(0(2(1(x1)))))
4(3(0(1(x1)))) -> 4(0(2(1(3(x1)))))
4(3(0(1(x1)))) -> 4(3(0(2(1(x1)))))
4(3(0(1(x1)))) -> 0(2(1(3(3(4(x1))))))
4(3(0(1(x1)))) -> 0(2(1(3(4(3(x1))))))
4(3(0(1(x1)))) -> 0(2(4(1(3(3(x1))))))
4(3(0(1(x1)))) -> 0(4(2(2(1(3(x1))))))
4(3(0(1(x1)))) -> 0(4(5(2(1(3(x1))))))
4(3(0(1(x1)))) -> 1(0(2(1(3(4(x1))))))
4(3(0(1(x1)))) -> 1(0(2(4(1(3(x1))))))
4(3(0(1(x1)))) -> 1(0(4(2(1(3(x1))))))
4(3(0(1(x1)))) -> 1(3(0(4(2(1(x1))))))
4(3(0(1(x1)))) -> 3(0(4(5(2(1(x1))))))
4(3(0(1(x1)))) -> 3(1(0(4(2(1(x1))))))
4(3(0(1(x1)))) -> 3(3(4(0(2(1(x1))))))
4(3(0(1(x1)))) -> 3(4(0(2(1(3(x1))))))
4(3(0(1(x1)))) -> 3(4(0(2(2(1(x1))))))
4(3(0(1(x1)))) -> 3(4(0(5(2(1(x1))))))
4(3(0(1(x1)))) -> 3(4(1(0(2(1(x1))))))
4(3(0(1(x1)))) -> 3(4(3(0(2(1(x1))))))
4(3(0(1(x1)))) -> 4(3(0(2(1(3(x1))))))
4(3(0(1(x1)))) -> 4(3(0(5(2(1(x1))))))
4(3(0(1(x1)))) -> 4(3(1(0(2(1(x1))))))
4(3(0(1(x1)))) -> 4(3(3(0(2(1(x1))))))
4(5(1(1(x1)))) -> 4(5(2(1(1(x1)))))
4(5(1(1(x1)))) -> 4(2(5(2(1(1(x1))))))
4(5(1(1(x1)))) -> 4(5(2(1(3(1(x1))))))
4(5(1(1(x1)))) -> 4(5(2(2(1(1(x1))))))
4(5(1(1(x1)))) -> 4(5(5(2(1(1(x1))))))
0(0(1(0(1(x1))))) -> 0(0(1(0(2(1(x1))))))
0(0(3(1(1(x1))))) -> 2(1(3(1(0(0(x1))))))
0(0(5(1(1(x1))))) -> 5(0(0(2(1(1(x1))))))
0(4(1(0(1(x1))))) -> 2(1(0(4(0(1(x1))))))
0(4(3(0(1(x1))))) -> 0(0(2(1(3(4(x1))))))
0(4(3(0(1(x1))))) -> 0(4(3(0(2(1(x1))))))
0(4(3(0(1(x1))))) -> 2(3(1(0(4(0(x1))))))
0(4(3(1(1(x1))))) -> 2(1(4(1(3(0(x1))))))
0(4(3(1(1(x1))))) -> 4(2(0(3(1(1(x1))))))
0(4(5(1(1(x1))))) -> 4(0(1(5(2(1(x1))))))
0(4(5(1(1(x1))))) -> 5(2(1(4(0(1(x1))))))
4(0(3(0(1(x1))))) -> 0(0(4(2(1(3(x1))))))
4(0(3(0(1(x1))))) -> 2(0(4(0(1(3(x1))))))
4(0(3(0(1(x1))))) -> 2(0(4(0(3(1(x1))))))
4(1(0(1(1(x1))))) -> 1(0(4(2(1(1(x1))))))
4(1(1(0(1(x1))))) -> 4(1(0(2(1(1(x1))))))
4(1(2(0(1(x1))))) -> 0(4(2(1(3(1(x1))))))
4(1(2(0(1(x1))))) -> 1(0(2(4(1(3(x1))))))
4(1(2(0(1(x1))))) -> 4(0(2(2(1(1(x1))))))
4(1(2(0(1(x1))))) -> 4(1(0(2(2(1(x1))))))
4(1(3(0(1(x1))))) -> 4(1(3(0(2(1(x1))))))
4(1(5(0(1(x1))))) -> 1(1(5(0(4(2(x1))))))
4(1(5(1(1(x1))))) -> 1(4(5(2(1(1(x1))))))
4(3(0(1(1(x1))))) -> 1(3(0(2(1(4(x1))))))
4(3(0(1(1(x1))))) -> 1(3(1(4(0(2(x1))))))
4(3(0(1(1(x1))))) -> 1(3(1(4(2(0(x1))))))
4(3(0(1(1(x1))))) -> 3(1(0(2(4(1(x1))))))
4(3(0(1(1(x1))))) -> 4(3(1(1(0(2(x1))))))
4(3(1(0(1(x1))))) -> 0(4(2(1(3(1(x1))))))
4(3(1(0(1(x1))))) -> 1(3(4(0(2(1(x1))))))
4(3(2(0(1(x1))))) -> 3(4(0(2(2(1(x1))))))
4(3(2(0(1(x1))))) -> 3(4(0(5(2(1(x1))))))
4(3(2(0(1(x1))))) -> 4(0(2(1(3(1(x1))))))
4(3(2(0(1(x1))))) -> 4(3(0(2(1(3(x1))))))
4(3(2(1(1(x1))))) -> 1(3(1(2(4(2(x1))))))
4(3(2(1(1(x1))))) -> 1(3(1(4(5(2(x1))))))
4(3(2(1(1(x1))))) -> 3(1(3(4(1(2(x1))))))
4(3(2(1(1(x1))))) -> 4(1(3(1(2(2(x1))))))
4(3(2(1(1(x1))))) -> 4(1(3(3(1(2(x1))))))
4(3(3(0(1(x1))))) -> 4(3(3(0(2(1(x1))))))
4(3(4(0(1(x1))))) -> 3(4(0(4(2(1(x1))))))
4(3(4(0(1(x1))))) -> 4(4(0(2(1(3(x1))))))
4(3(5(0(1(x1))))) -> 0(5(2(3(1(4(x1))))))
4(3(5(0(1(x1))))) -> 1(3(0(2(5(4(x1))))))
4(3(5(0(1(x1))))) -> 1(3(0(4(2(5(x1))))))
4(3(5(0(1(x1))))) -> 1(3(4(0(5(2(x1))))))
4(3(5(0(1(x1))))) -> 3(1(0(4(2(5(x1))))))
4(3(5(0(1(x1))))) -> 3(1(5(0(4(2(x1))))))
4(3(5(0(1(x1))))) -> 3(4(0(2(1(5(x1))))))
4(3(5(0(1(x1))))) -> 3(4(1(5(0(2(x1))))))
4(3(5(0(1(x1))))) -> 3(5(1(0(4(2(x1))))))
4(3(5(0(1(x1))))) -> 4(3(0(2(1(5(x1))))))
4(3(5(0(1(x1))))) -> 5(1(3(4(0(2(x1))))))
4(3(5(1(1(x1))))) -> 1(4(5(2(1(3(x1))))))
4(3(5(1(1(x1))))) -> 3(1(1(5(4(2(x1))))))
4(3(5(1(1(x1))))) -> 3(1(4(5(2(1(x1))))))
4(3(5(1(1(x1))))) -> 4(1(3(1(3(5(x1))))))
4(3(5(1(1(x1))))) -> 4(1(5(2(1(3(x1))))))
4(3(5(1(1(x1))))) -> 4(3(1(5(2(1(x1))))))
4(4(1(0(1(x1))))) -> 4(4(1(0(2(1(x1))))))
4(4(3(0(1(x1))))) -> 0(4(4(2(1(3(x1))))))
4(4(3(0(1(x1))))) -> 4(0(2(1(3(4(x1))))))
4(4(3(0(1(x1))))) -> 4(3(4(0(2(1(x1))))))
4(4(3(0(1(x1))))) -> 4(4(3(0(2(1(x1))))))
4(5(1(0(1(x1))))) -> 0(5(1(3(4(1(x1))))))
4(5(1(0(1(x1))))) -> 0(5(4(1(3(1(x1))))))
4(5(1(0(1(x1))))) -> 1(0(4(5(2(1(x1))))))
4(5(1(0(1(x1))))) -> 4(0(5(2(1(1(x1))))))
4(5(1(0(1(x1))))) -> 4(5(1(0(2(1(x1))))))
4(5(1(0(1(x1))))) -> 5(1(0(2(4(1(x1))))))
4(5(1(0(1(x1))))) -> 5(4(1(0(2(1(x1))))))
4(5(1(1(1(x1))))) -> 4(5(2(1(1(1(x1))))))
4(5(3(0(1(x1))))) -> 0(2(1(3(4(5(x1))))))
4(5(3(0(1(x1))))) -> 0(5(2(1(3(4(x1))))))
4(5(3(0(1(x1))))) -> 0(5(2(4(3(1(x1))))))
4(5(3(0(1(x1))))) -> 0(5(4(2(1(3(x1))))))
4(5(3(0(1(x1))))) -> 1(0(5(1(3(4(x1))))))
4(5(3(0(1(x1))))) -> 1(5(0(3(3(4(x1))))))
4(5(3(0(1(x1))))) -> 2(1(4(5(0(3(x1))))))
4(5(3(0(1(x1))))) -> 2(4(1(3(5(0(x1))))))
4(5(3(0(1(x1))))) -> 3(0(4(5(2(1(x1))))))
4(5(3(0(1(x1))))) -> 4(0(3(1(5(2(x1))))))
4(5(3(0(1(x1))))) -> 4(0(3(3(5(1(x1))))))
4(5(3(0(1(x1))))) -> 4(0(5(4(1(3(x1))))))
4(5(3(0(1(x1))))) -> 4(1(3(5(0(3(x1))))))
4(5(3(0(1(x1))))) -> 4(1(3(5(5(0(x1))))))
4(5(3(0(1(x1))))) -> 4(2(5(0(3(1(x1))))))
4(5(3(0(1(x1))))) -> 4(5(2(0(3(1(x1))))))
4(5(3(0(1(x1))))) -> 5(0(3(1(4(1(x1))))))
4(5(3(0(1(x1))))) -> 5(0(3(4(4(1(x1))))))
4(5(3(0(1(x1))))) -> 5(1(3(0(3(4(x1))))))
4(5(3(0(1(x1))))) -> 5(2(1(3(4(0(x1))))))
4(5(3(0(1(x1))))) -> 5(2(4(1(3(0(x1))))))
4(5(3(0(1(x1))))) -> 5(3(0(4(2(1(x1))))))
4(5(3(0(1(x1))))) -> 5(4(1(3(0(1(x1))))))
4(5(3(0(1(x1))))) -> 5(4(1(3(2(0(x1))))))
4(5(3(0(1(x1))))) -> 5(4(3(0(2(1(x1))))))
4(5(3(1(1(x1))))) -> 2(4(1(3(1(5(x1))))))
4(5(3(1(1(x1))))) -> 4(5(2(1(3(1(x1))))))
4(5(3(1(1(x1))))) -> 5(1(3(4(1(2(x1))))))
4(5(3(1(1(x1))))) -> 5(2(1(4(1(3(x1))))))
4(5(3(1(1(x1))))) -> 5(4(2(1(3(1(x1))))))
4(5(5(1(1(x1))))) -> 5(5(2(1(1(4(x1))))))
4(5(5(1(1(x1))))) -> 5(5(2(4(1(1(x1))))))
Proof:
Bounds Processor:
bound: 2
enrichment: match
automaton:
final states: {6,5}
transitions:
51(55) -> 56*
51(134) -> 135*
51(39) -> 40*
51(201) -> 202*
51(151) -> 152*
51(183) -> 184*
51(153) -> 154*
51(143) -> 144*
51(88) -> 89*
51(145) -> 146*
51(130) -> 131*
21(187) -> 188*
21(67) -> 68*
21(47) -> 48*
21(174) -> 175*
21(79) -> 80*
21(69) -> 70*
21(49) -> 50*
21(81) -> 82*
21(41) -> 42*
21(133) -> 134*
21(73) -> 74*
21(38) -> 39*
21(200) -> 201*
21(105) -> 106*
41(197) -> 198*
41(92) -> 93*
41(219) -> 220*
41(89) -> 90*
41(221) -> 222*
41(19) -> 20*
41(211) -> 212*
41(213) -> 214*
41(173) -> 174*
41(68) -> 69*
41(195) -> 196*
41(185) -> 186*
41(135) -> 136*
11(70) -> 71*
11(172) -> 173*
11(57) -> 58*
11(37) -> 38*
11(27) -> 28*
11(199) -> 200*
11(169) -> 170*
11(159) -> 160*
11(94) -> 95*
11(29) -> 30*
11(14) -> 15*
11(186) -> 187*
11(161) -> 162*
11(131) -> 132*
11(91) -> 92*
11(21) -> 22*
11(16) -> 17*
11(198) -> 199*
11(18) -> 19*
31(15) -> 16*
31(162) -> 163*
31(107) -> 108*
31(17) -> 18*
31(171) -> 172*
31(121) -> 122*
31(71) -> 72*
31(123) -> 124*
31(113) -> 114*
31(93) -> 94*
31(115) -> 116*
31(95) -> 96*
42(237) -> 238*
12(257) -> 258*
12(232) -> 233*
12(234) -> 235*
12(251) -> 252*
12(236) -> 237*
12(253) -> 254*
12(243) -> 244*
12(245) -> 246*
00(2) -> 5*
00(4) -> 5*
00(1) -> 5*
00(3) -> 5*
32(233) -> 234*
32(235) -> 236*
10(2) -> 1*
10(4) -> 1*
10(1) -> 1*
10(3) -> 1*
20(2) -> 2*
20(4) -> 2*
20(1) -> 2*
20(3) -> 2*
30(2) -> 3*
30(4) -> 3*
30(1) -> 3*
30(3) -> 3*
40(2) -> 6*
40(4) -> 6*
40(1) -> 6*
40(3) -> 6*
50(2) -> 4*
50(4) -> 4*
50(1) -> 4*
50(3) -> 4*
1 -> 213,151,121,79,27
2 -> 197,143,113,67,14
3 -> 219,153,123,81,29
4 -> 211,145,115,73,21
14 -> 245*
15 -> 133,37
17 -> 185,47
20 -> 220,212,222,214,198,200,57,6
21 -> 251*
22 -> 15*
27 -> 232*
28 -> 15*
29 -> 243*
30 -> 15*
37 -> 253*
38 -> 221,171,169
39 -> 49*
40 -> 159,55,41,19
42 -> 19*
48 -> 195,39
50 -> 39*
56 -> 19*
58 -> 220,222,214,198,200,6
68 -> 105,91,88
69 -> 130*
72 -> 57*
74 -> 68*
80 -> 68*
82 -> 68*
90 -> 70*
92 -> 107*
95 -> 183*
96 -> 220,198,6
106 -> 16*
108 -> 17*
114 -> 16*
116 -> 16*
122 -> 16*
124 -> 16*
132 -> 94*
135 -> 161*
136 -> 94*
144 -> 15*
146 -> 15*
152 -> 15*
154 -> 15*
160 -> 19*
163 -> 19*
169 -> 257*
170 -> 38*
175 -> 212,198,6
184 -> 212,198,6
188 -> 183*
196 -> 183*
202 -> 183*
212 -> 198*
214 -> 198*
220 -> 198*
222 -> 200*
238 -> 222,200
244 -> 233*
246 -> 233*
252 -> 233*
254 -> 233*
258 -> 233*
problem:
Qed